$\forall$$T$:Type, ${\it eq}$, $r$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$), $x$:$T$, $L$:($T$ List). insert{-}by(${\it eq}$;$r$;$x$;$L$) $\in$ ($T$ List)